Theorem ralrn 7122

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6935	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6982	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2747	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3100	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5428	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  Vcvv 3488  ran crn 5701   Fn wfn 6568  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-fv 6581

This theorem is referenced by:  ralrnmptw  7128  ralrnmpt  7130  cbvfo  7325  isoselem  7377  indexfi  9430  ordtypelem9  9595  ordtypelem10  9596  wemapwe  9766  numacn  10118  acndom  10120  rpnnen1lem3  13044  fsequb2  14027  limsuple  15524  limsupval2  15526  climsup  15718  ruclem11  16288  ruclem12  16289  prmreclem6  16968  imasaddfnlem  17588  imasvscafn  17597  cycsubgcl  19246  ghmrn  19269  ghmnsgima  19280  pgpssslw  19656  gexex  19895  dprdfcntz  20059  znf1o  21593  frlmlbs  21840  lindfrn  21864  ptcnplem  23650  kqt0lem  23765  isr0  23766  regr1lem2  23769  uzrest  23926  tmdgsum2  24125  imasf1oxmet  24406  imasf1omet  24407  bndth  25009  evth  25010  ovolficcss  25523  ovollb2lem  25542  ovolunlem1  25551  ovoliunlem1  25556  ovoliunlem2  25557  ovoliun2  25560  ovolscalem1  25567  ovolicc1  25570  voliunlem2  25605  voliunlem3  25606  ioombl1lem4  25615  uniioovol  25633  uniioombllem2  25637  uniioombllem3  25639  uniioombllem6  25642  volsup2  25659  vitalilem3  25664  mbfsup  25718  mbfinf  25719  mbflimsup  25720  itg1ge0  25740  itg1mulc  25759  itg1climres  25769  mbfi1fseqlem4  25773  itg2seq  25797  itg2monolem1  25805  itg2mono  25808  itg2i1fseq2  25811  itg2gt0  25815  itg2cnlem1  25816  itg2cn  25818  limciun  25949  plycpn  26349  hmopidmchi  32183  hmopidmpji  32184  rge0scvg  33895  mclsax  35537  mblfinlem2  37618  ismtyhmeolem  37764  nacsfix  42668  fnwe2lem2  43008  gneispace  44096  climinf  45527  liminfval2  45689