Theorem ralrn 7042

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 6855	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6903	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2736	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3076	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5360	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3444  ran crn 5632   Fn wfn 6494  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6452  df-fun 6501  df-fn 6502  df-fv 6507

This theorem is referenced by:  ralrnmptw  7048  ralrnmpt  7050  cbvfo  7246  isoselem  7298  indexfi  9287  ordtypelem9  9455  ordtypelem10  9456  wemapwe  9626  numacn  9978  acndom  9980  rpnnen1lem3  12914  fsequb2  13917  limsuple  15420  limsupval2  15422  climsup  15612  ruclem11  16184  ruclem12  16185  prmreclem6  16868  imasaddfnlem  17467  imasvscafn  17476  cycsubgcl  19120  ghmrn  19143  ghmnsgima  19154  pgpssslw  19528  gexex  19767  dprdfcntz  19931  znf1o  21493  frlmlbs  21739  lindfrn  21763  ptcnplem  23541  kqt0lem  23656  isr0  23657  regr1lem2  23660  uzrest  23817  tmdgsum2  24016  imasf1oxmet  24296  imasf1omet  24297  bndth  24890  evth  24891  ovolficcss  25403  ovollb2lem  25422  ovolunlem1  25431  ovoliunlem1  25436  ovoliunlem2  25437  ovoliun2  25440  ovolscalem1  25447  ovolicc1  25450  voliunlem2  25485  voliunlem3  25486  ioombl1lem4  25495  uniioovol  25513  uniioombllem2  25517  uniioombllem3  25519  uniioombllem6  25522  volsup2  25539  vitalilem3  25544  mbfsup  25598  mbfinf  25599  mbflimsup  25600  itg1ge0  25620  itg1mulc  25638  itg1climres  25648  mbfi1fseqlem4  25652  itg2seq  25676  itg2monolem1  25684  itg2mono  25687  itg2i1fseq2  25690  itg2gt0  25694  itg2cnlem1  25695  itg2cn  25697  limciun  25828  plycpn  26230  hmopidmchi  32130  hmopidmpji  32131  rge0scvg  33932  mclsax  35549  mblfinlem2  37645  ismtyhmeolem  37791  nacsfix  42693  fnwe2lem2  43033  gneispace  44116  climinf  45597  liminfval2  45759